Definitions	FIncr, x:A. B(x), t  T, , WellFnd{i}(A;x,y.R(x;y)), x(s), {T}, T, True, AB, A, False, P  Q, Prop, ij, x f y, i=j, P  Q, if b t else f fi, {i...}, a  b
Lemmas	int upper wf, eq int eq false elim sqequal, eq int eq true elim sqequal, bool cases sqequal, eq int wf, nat properties, ge wf, le wf, nat wf